#pragma once

#include "clause.h"
#include <list>
#include <algorithm>

namespace solver
{
	class decision
	{
	public:
		int selected_literal;
		std::vector<literal> literals;
	};

	typedef decision *pdecision;

	class decision_string : public std::vector<literal>
	{
		bool is_c_str;

	public:

		bool sorted;

		decision_string() : is_c_str(false), sorted(true)
		{

		}

		decision_string( const char *mystr ) : is_c_str(true), sorted(false)
		{
			literal lit;
			int val = 1;
			bool star = false;

			while (*mystr)
			{

				switch (*mystr) 
				{
				case 'A':
				case 'B':
				case 'C':
				case 'D':
				case 'E':
				case 'F':
				case 'G':
				case 'H':
				case 'I':
				case 'J':
				case 'K':
				case 'L':
				case 'M':
				case 'N':
				case 'O':
				case 'P':
				case 'Q':
				case 'R':
				case 'S':
				case 'T':
				case 'U':
				case 'V':
				case 'W':
				case 'X':
				case 'Y':
				case 'Z':
					lit.ref = *mystr;
					lit.val = val;
					lit.star = star;
					val = 1;
					star = false;
					push_back(lit);
					break;
				case '*':
					star = true;
					val = -1;
					break;
				case '!':
					val = !val;
					break;
				}

				if (*mystr) 
				{
					mystr++;
				}
			}
		}

		std::string to_string()
		{
			std::string x = "";
			if (is_c_str) {
				for (auto& dcdest : *this)
				{
					if (dcdest.star) 
					{
						x += "*";
					}
					else if (!dcdest.val)
					{
						x += "!";
					}
					std::string temp(1,(char)dcdest.ref);
					x += temp;
				}
			}
			return x;
		}

		bool contains(const literal& dc) const
		{
			bool found = false;
			for (auto& dcdest : *this) {
				if (dc == dcdest) {
					return true;
				}
			}
			return found;
		}

		bool contains(decision_string* dec) const
		{
			for (auto ici = dec->begin(); ici != dec->end(); ici++)
			{
				bool found = contains(*ici);
				if (!found)
					return false;
			}
			return true;
		}

		bool contains(decision_string& dec) const
		{
			for (auto&ic : dec)
			{
				bool found = contains(ic);
				if (!found)
					return false;
			}
			return true;
		}

		bool contained(std::vector<int>& index)
		{
			for (auto& ic : *this) 
			{
				if (index[ic.ref] != ic.val) 
				{
					return false;
				}
			}
			return true;
		}

		bool add(literal l)
		{
			sorted = false;
			bool success = conflict_free(l);
			if (success)
			{
				std::vector<literal>::push_back(l);
			}
			return success;
		}

		bool add_sorted(const literal& l, bool& conflicted)
		{
			bool found, notfound;
			bool nonconflicted = exists_conflict_free(l, found);

			notfound = !found;
			if (notfound) {
				if (!sorted)
					sort();
				this->insert
				(
					std::upper_bound(this->begin(), this->end(), l),
					l
				);
			}
			conflicted = nonconflicted;
			return notfound;
		}

		bool add_sorted_conflicted(const literal& l)
		{
			bool notfound = !contains(l);
			if (notfound) {
				if (!sorted)
					sort();
				this->insert
				(
					std::upper_bound(this->begin(), this->end(), l),
					l
				);
			}
			return notfound;
		}

		static bool clear_literal_pointers(std::vector<literal *>& indeces)
		{
			int iend = indeces.size();
			if (iend == 0)
				return false;

			literal **p = indeces.data();
			literal **plast = p + iend;

			while (p < plast)
			{
				auto tp = *p;
				if (tp) 
				{
					(tp)->val = 0;
				}
				p++;
			}

			return true;
		}

		static bool increment_literal_pointers(std::vector<literal *>& indeces, int max_value)
		{
			int iend = indeces.size();
			if (iend == 0)
				return false;

			literal **pbase = indeces.data();
			literal **pend = pbase + iend - 1;
			literal **p = pend;

			bool found = false;
			do {
				auto v = (*p);
				if (v->val < max_value) {
					v->val++;
					p++;
					while (p <= pend)
					{
						auto vn = (*p);
						vn->val = 0;
						p++;
					}
					found = true;
					break;
				}
				p--;
			} while (p >= pbase);

			return found;
		}

		static int find_literal_pointers(decision_string& target, decision_string& search, std::vector<literal *>& litpointers)
		{
			int count = 0;

			if (!search.size() || !target.size())
			{
				return count;
			}

			if (!target.sorted)
				target.sort();

			if (!search.sorted)
				search.sort();

			litpointers.resize(search.size());

			literal *targetbase = target.data();
			literal *targetend = targetbase + target.size();

			const literal *cmpbase = search.data();
			const literal *cmpend = cmpbase + search.size();
			const literal *cmp = cmpbase;

			literal **destbase = litpointers.data();
			literal **destend = destbase + litpointers.size();
			literal **dest = destbase;

			for (dest = destbase; dest <= destbase; dest++)
			{
				*dest = nullptr;
			}

			dest = destbase;
			for (cmp = cmpbase; cmp <= cmpend; cmp++)
			{
				while (targetbase->ref < cmp->ref)
				{
					targetbase++;
				}
				if (targetbase->ref == cmp->ref)
				{
					*dest = targetbase;
					dest++;
					count++;
				}
			}

			return count;
		}

		bool conflict_free(literal l)
		{
			bool success = true;

			for (auto& v : *this)
			{
				if (v.ref == l.ref && v.val != l.val)
				{
					success = false;
					break;
				}
			}

			return success;
		}

		bool exists_conflict_free(literal l, bool& found)
		{
			bool success = true;
			found = false;
			for (auto& v : *this)
			{
				if (v.ref == l.ref)
				{
					found = true;
					success = (v.val == l.val);
					break;
				}
			}

			return success;
		}

		bool conflict_free(pdecision dec)
		{
			int s = dec->literals.size();

			for (auto& dc : dec->literals)
			{
				bool found;
				bool is_free = exists_conflict_free(dc, found);
				if (!found)
					return true;
				if (!is_free)
					return false;
			}

			return true;
		}

		decision_string remove_literal(literal lit)
		{
			decision_string dsx;
			for (auto ch : *this)
			{
				if (ch != lit)
				{
					dsx.add(ch);
				}
			}
			return dsx;
		}
		
		decision_string *clone()
		{
			decision_string *ds = new decision_string(*this);
			return ds;
		}

		void sort()
		{
			std::sort(begin(), end(), [](const literal& a, const literal& b) {
				return a.ref < b.ref && a.val < b.val;
			});
			sorted = true;
		}

		static int compare(const decision_string& srcA, const decision_string& srcB)
		{
			auto srcAi = srcA.begin();
			auto srcBi = srcB.begin();

			while (srcAi != std::end(srcA) && srcBi != std::end(srcB))
			{
				if (srcAi->ref < srcBi->ref) {
					return -1;
				}
				else if (srcAi->ref > srcBi->ref) {
					return 1;
				}
				else if (srcAi->val < srcBi->val) {
					return -1;
				}
				else if (srcAi->val > srcBi->val) {
					return 1;
				}
				srcAi++;
				srcBi++;
			}

			if (srcAi == std::end(srcA) && srcBi == std::end(srcB))
			{
				return 0;
			}

			if (srcAi == std::end(srcA) && srcBi != std::end(srcB))
			{
				return -1;
			}

			return 1;
		}

		static int comparei(const decision_string& srcA, const decision_string& srcB)
		{
			auto srcAi = srcA.begin();
			auto srcBi = srcB.begin();

			while (srcAi != std::end(srcA) && srcBi != std::end(srcB))
			{
				if (srcAi->ref < srcBi->ref) {
					return -1;
				}
				else if (srcAi->ref > srcBi->ref) {
					return 1;
				}
				srcAi++;
				srcBi++;
			}

			if (srcAi == std::end(srcA) && srcBi == std::end(srcB))
			{
				return 0;
			}
			
			if (srcAi == std::end(srcA) && srcBi != std::end(srcB))
			{
				return -1;
			}

			return 1;
		}

		static bool compare_strick_weak_orderi(const decision_string& srcA, const decision_string& srcB)
		{
			return comparei(srcA, srcB) < 0;
		}

		static bool compare_strick_weak_orderi(const decision_string* srcA, const decision_string* srcB)
		{
			return compare_strick_weak_orderi(*srcA, *srcB);
		}

		bool operator < (const decision_string& srcA)
		{
			return decision_string::compare(*this, srcA) < 0;
		}

		bool operator <= (const decision_string& srcA)
		{
			return decision_string::compare(*this, srcA) <= 0;
		}

		bool operator == (const decision_string& srcA)
		{
			return decision_string::compare(*this, srcA) == 0;
		}

		bool operator >= (const decision_string& srcA)
		{
			return decision_string::compare(*this, srcA) >= 0;
		}

		bool operator > (const decision_string& srcA)
		{
			return decision_string::compare(*this, srcA) > 0;
		}

	};

	typedef decision_string *pdecision_string;

}
